IC chips generally comprise a plurality of cells. Each cell may include one or more circuit elements such as transistors, capacitors and other basic circuit elements, which are interconnected in a standardized manner to perform a specific function.
Timing Driven Resynthesis described in U.S. Pat. No. 6,564,361, filed Oct. 2, 2000 has been used to change the chip design step by step, making the improvements of the chip locally. The main idea of the local resynthesis is to consecutively examine the cell trees of a chip for the necessity of optimization, and then to organize the chosen trees as local tasks for the resynthesis that follows. All necessary information about the tree neighborhood (neighboring cells, capacities, delays, etc.) is first collected. Next, local optimization procedures work with this information only. No additional information about the chip structure is required. A net may include a wire and a set of cell pins connected to the wire.
Within the logical resynthesis, ordinary logical cells are considered, i.e. those cells with one output pin constructed using standard logical gates NOT, AND, OR. A logical tree is a tree formed from ordinary logical cells. Inside a logical tree, except the root (or root cell) of the tree, the output pin of each cell of the tree is connected to exactly one other input pin, and this one other input pin is a pin of a cell of the logical tree. In contrast, the output pin of the root may be connected to any number of cell input pins. All cells connected to the output pin of the root of a tree may not belong to the tree, and the cells are not necessarily logical. An input pin of a cell of the tree may be connected to the power or the ground. Moreover, a cell input pin of a tree may be connected to a cell outside the tree, and the cell input pin may be called the entrance of the tree.
FIG. 1 shows an exemplary logical tree 100. The tree 100 may include 6 cells drawn inside the dotted rectangle. All entrances of the tree 100 may be enumerated by assigning variables xn to the entrances. In addition, identical variables may be assigned to entrances connected through a wire because the input values of these entrances are always the same. As shown, for example, the variable x1 is assigned to the first input pin of the cell ND3C and to the first input pin of the cell ENB, the variable x2 is assigned to the second input pin of the cell ENB and to the first input pin of the cell NR2A, and the variable x3 is assigned to the input pin of the cell N1C.
A logical tree may be presented as a logical expression on the technology basis. For instance the tree 100 shown in FIG. 1 may be presented as the following logical expression:AND2B(ND3C(x1, 1, ENB(x1, x2)), N1A(NR2A(x2, N1C(x3)))).One goal of the logical resynthesis is to change a logical expression into a logically equivalent one, which is better with respect to a given estimator.
The method of identities is a known method to find logically equivalent formulas and assumes that unification substitutions for formulas may be found. Let A=B be an identity, i.e. a pair of equivalent formulas on some bases. For example, and2(not(x1), x2)=not (or2(not(x2), x1)) is an identity. Let C be a formula on a basis, for example, and2(not(or2(x3, x4)), not (x5)). If A(x1, . . . , xn) and A(D1, . . . , Dn)=C, where D1, . . . , Dn are formulas, then the substitution xi→Di (i=1, . . . , n) may be called unification substitution for formulas A and C. To apply the identity A=B to the formula C, unification substitution for formulas A and C need be found. There are 2 unification substitutions for formulas and2(not(x1), x2) and and2(not(or2(x3, x4)), not (x5)):                a) x1→or2(x3, x4), x2→not(x5),        b) x1→x5, x2→not(or2(x3, x4)).Therefore, there are two results of application of the identity and2(not(x1), x2)=not(or2(not(x2), x1)) to formula and2(not(or2(x3, x4)), not(x5)) as follows:        a) not(or2(not(not(x5)), or2(x3, x4))),        b) not(or2(not(not(or2(x3, x4))), x5)).        
The application of an identity to a formula has been described in U.S. Pat. No. 6,543,032, filed Oct. 2, 2000 and in U.S. Pat. No. 6,637,011, filed Oct. 2, 2000, and has been used for logical resynthesis in LSI Logic Corp.'s internal synthesis tool MRS to minimize the path delays and eliminate the ramptime violations (see e.g., U.S. Pat. No. 6,564,361, filed Oct. 2, 2000). However, if there are several unification substitutions, then the best substitution need be selected to minimize the path delays or eliminate the ramptime violations.
Therefore, it would be desirable to provide a method and apparatus to quickly find an optimal unification substitution for formulas in a technology library.